open util/integer
open util/natural as natural
private open util/ordering[Natural] as ord


abstract sig Element {
	we: Natural
} 
fact {
	all e:Element | some a:Arch | e in a.elements
}

one sig E1 extends Element {} { we = One.next }
one sig E2 extends Element {} { we = One.next.next }

sig Arch {
	elements: set Element,
	wa: Natural
} 


fact {
	all a:Arch  | #ord/prevs[a.wa] = (sum e: a.elements | #ord/prevs[e.we]) 
}


run {(all n:(Element.we+Arch.wa) | natural/gt[n,One]) and some Arch and (all b:Arch | #(b.elements) > 1)} for 4 Element, 1 Arch, 6 Natural, 10 int
